the_w:World, i:Id, t:. first(<i,t>)   

latex

Definitions	x:A. B(x), , t  T, first(e), Y, if b t else f fi, i=j, time(e), true, loc(e), 2of(t), 1of(t), AB, A, P  Q, False, ij, Prop
Lemmas	nat wf, Id wf, world wf, btrue wf, ifthenelse wf, eq int wf, bool wf, w-isnull wf, w-a wf, le wf, bfalse wf, nat properties, ge wf